Issue4638-4.agda:11,1-12,11
Cannot branch on erased argument of datatype D
when checking the definition of f
